Nuprl Definition : ecl-add-throw 11,40

ecl-add-throw(A; m)
== spreadn(A;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.<Ta
== spreadn(, ksa
== spreadn(, ia
== spreadn(, ga
== spreadn(, n,x. if (n = m) then bor((ha(0,x)); (ha(n,x))) else band(0 <z n; (ha(n,x))) fi 
== spreadn(, aa
== spreadn(, if (m = 0) then ea else s-insert(m; ea) fi >) 
latex


Definitionsspreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), bor(p; q), band(p; q), i <z j, if b then t else f fi , (i = j), s-insert(x; l)
FDL editor aliasesecl-add-throw

origin